perm filename ENT.LSP[LSP,JRA] blob sn#211843 filedate 1976-04-20 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.SS(Computation,,R3:)
C00011 00003	We can add dummy variables to, and also permute, and identify variables
C00021 ENDMK
C⊗;
.SS(Computation,,R3:)
In describing a process of computation for a theory,
what we are attempting to do is establish a decision procedure.
What we would like is an algorithm which, given any wff of the theory,
will tell us whether or not that wff is provable. For propositional logic
we described such an algorithm in terms of complementary literal elimination.
We could instead have described an algorithm for constructing truth tables
with the same result.  We had both completeness and decibability.

In the case of predicate calculus we again established completeness, but our
algorithm was only a partial  decision procedure. Given a theorem it would indeed
tells us we had a theorem, but given a non-theorem it might let us know (by
closing out) or the computation may continue infinitely. We have not  shown
that there does not exist a decision procedure for Predicate calculus, only that we
haven't found one.

We shall prove that there is no decision procedure for determining theorem-hood
of an arbitrary wff of ENT.
Undecidability for Predicate
calculus follows since it can be shown that given a decidable theory, the addition
of a finite number of axioms also results in a decidable theory.
If there did exist a decision procedure, ?f, it would have to be a total function
over all wffs of ENT whose output ?f(?A) for any ?A tells us whether or not
?A is provable. For instance
.BEGIN INDENT 10,10;

?f(?A) = 0  if ?A is provable

?f(?A) = 1  if ?A is not provable
.END
We'd like to know something about the structure of ?f. We know it must be an
algorithm; given input it chugs through a precise  set of steps to compute
output.  We say it is a %3computable function%1. G⊗odel, elaborating
on an idea of Herbrand, formalized the concept of total computable functions in
general recursive function theory.  Every total computable function can be expressed
as a general recursive function. Thus  ?f is (or could be expressed as) generally
recursive. It turns out that all generally recursive functions (and sets) are
representable in the formal system of ENT; this will give us  
a contradiction to the existence of ?f.

.BEGIN nofill;
Defs.1. The following functions are called %3initial functions%1:
	I   The zero functon: πZ(πx) = π0 for all πx.
	II  The successor function (or next): πN(πx) = πx+π1 for all πx.
	III The projection functions: πUni(πx1n) = πxi for all πx1n.

      2.The following are rules for obtaining new functions from given functions:
	IV  Substitution: πf(πx1n) = πg(πh1(πx1n), ..., πhm(πx1n))
	    πf is said to be obtained by substitution from the functions:
		πg(πy1, ...πym), πh1(πx1n), ..., πhm(πx1n)

        V   Recursion:
		πf(πx1n,π0) = πg(πx1n)
		πf(πx1n,πy+π1) = πh(πx1n, πy, πf(πx1n, πy))
            in the case when πn = π0:
		πf(π0) = πk   (where πk is a fixed integer)
		πf(πy+π1) = πh(πy, πf(πy))
.begin indent 13,13;fill
We say that πf is obtained from πg and πh (or in the case πn=π0, from πh alone)
by recursion. The %3parameters%* of the recursion are πx1n. Note that
πf is well-defined: the value of πf(πx1n,π0) is given by the first
equation, and if we already know that the value of πf(πx1n,πy), then
we obtain πf(πx1n,#πy+π1) by the second equation.
.end

.begin indent  9,13;fill;
       	VI  ?m-operator: assume that πg(πx1n, πy) is a function
such that for any πx1n there is at least one πy such that πg(πx1n,πy) =π0.
We denote by ?mπy(πg(πx1n,πy)=π0) that least number πy such that πg(πx1n)#=#π0
In geneal, for any relation πR(πx1n,πy), we denote by ?mπyπR(πx1n,πy) the
least πy such that πR(πx1n,πy) is true, if there is any πy at all such
that πR(πx1n,πy) holds.
Let πf(πx1n)#=#?mπy(πg(πx1n,#πy)#=#π0). Then πf is said to be obtained from πg
by means of the ?m-operator, if the given assumption about πg holds; i.e., for
any πx1n, there is at least one πy such that πg(πx1n#πy)#=#π0.
.end

	
.begin indent 7,7;fill;
     3. A function is said to be %3primitive recursive%1 iff it can be obtained
from the initial functions by any finite number of substitutions (IV) 
and recursions (V); i.e., if there is a finite sequence of functions, πf0,#...,πfn,
such that πf#=#πfn, and, for any π0≤πi≤πn, either πfi is an initial function
or πfi is obtained from preceding functions in the sequence by an application of
Rule IV (Substitution) or Rule V (Recursion).

4. A function πf is said to be %3recursive%* (or generally recursive) iff it can be 
obtained from the initial functions by a finite number of applications
of Substitution, Recursion, and the ?m-operator (VI). Clearly, every primitive
recursive function is recursive; it can be shown that the converse is false.
.end
.end

1. If πR(πx1n) is a relation, then the %3characteristic function%1, πCR(πx1n), is defined as
follows:
.begin tabit2(25,40);
\πCR(πx1n) =\π0 if πR(πx1n) is true
\\π1 if πR(πx1n) is false
.end

If πA is a set of natural numbers, then the characteristic function πCA(πx) is
defined as follows.

.BEGIN TABIT2(30,47);
\πCA(πx)\π0 if πxεπA
\\π1 if πx%5N%1πA
.end

2. A relation πR(πx1n) is said to be primitve recursive (or recursive) iff
its characteristic function is primitve recursive (recursive). In particular,
a set πA of natural numbers is primitive recursive (recursive) iff its
characteristic function is.

3. We shall show that the class of recursive functions  is identical wth the class
of functions representable in ENT.
We can add dummy variables to, and also permute, and identify variables
in any primitive recursive or recursive function, obtaining a function of the
same type.

.begin fill;indent 0,10;
.group
%7LEMMA 5%1 Let πg(πy1, ...,πyk) be primitve recursive (or recursive).
Let πx1n be distinct variables, and for π1≤πi≤πk, let πzi be one of πx1n.
.apart;
.group;
The function πf(πx1n)#=#πg(πx1,#...,#πxk) is primitive recursive (or recursive).

Proof: Let πzi = %3x%4j1%1 (where π1≤%3j1%1≤πn). Then πzi = %3U%8n%4jk%1(πx1n);
thus πf(πx1n)#=#πg(%3U%8n%4j1%1(πx1n);#%3U%8n%4j2%1(πx1n);#...,#%3U%8n%4jk%1(πx1n))
and therefore πf is PR (r R), snce is arises from the base functions and
substitutions.

%7COR. 5.1%1 a) The zero function πZ%4n%1(πx1n)#=#π0 is PR.
.END
.BEGIN INDENT 10,10;
b) The constant function πC%8n%4k(πx1n) = πk, where πk is sme fixed integer,
is PR.

c) The substitution rule (IV) can be extended to the case  where each πhi
may be a function of some but not necessarily all of the variables. Likewise,
in the Recursion rule (V), the function πg may not involve all of the varaibles,
πx1n; and πh may not involve all of the variables πx1n,πy or πf(πx1n,#πy).
.end

.BEGIN TABIT3(10,30,50);
%7LEMMA 6%1 The following functions are all PR:
\a) πx+πy\b) πx⊗xπy\c) πx%8y%1
\d) πx+πy\e) |πx-πy|\f) πx!
\g) %3min%1(πx,πy)\h) %3min%1(πx1n)\i) %3max%1(πx,πy)
\j) %3max%1(πx1n)\k) %gd%1(πx) πx-π1 if πx>π0
\\     π0 if πx=π0

\l) %3sg%1(πx)  π0 if πx=π0\m) %3nsg%1(πx)  π1 if πx=π0
\          π1 if πx≠π0\       π0 if πx≠0

n) %3rm%1(πx,πy) = remainder upon division of πy by πx.
o) %3qt%1(πx,πy) = quotient upon division of πy by πx.
.end
.begin indent 0,10;
Proof: proof of a) by the Recursion Rule:
.begin tabit2(10,35);select 3;

\x + 0 = x\f(x,0) = U%81%41%3(x)
\           %1or%3
\x+(y+1) = N(x+y)\f(x,N(y)) = N(f(x,y))

%1proof of b)%3

\x⊗x%30 = 0\g(x,0) = Z(x)
\           %1or%3
\x⊗x%3(y+1) = (x⊗x%3y)+x\g(x,N(y)) = f(g(x,y), x)
\\   %1where πf is the addition function.

%1proof of n)%3

\rm(x,0) = 0
\rm(x,y+1) = N(rm(x,y))⊗x%3sg(|x-N(rm(x,y))|)
.end
See Mendelson for the proofs of the other parts.
.end

.BEGIN TABIT2(10,25);
Definitions:
\%GS%4y<z%1πf(πx1n,πy)\π0 if %3z = 0%1
\\πf(πx1n,π0)+ ... +πf(πx1n,πz-π1) if πz≥π0

\%gS%4y≤z%1πf(πx1n,πy) = %gS%4y<z+1%1πf(πx1n,πy)

\%GP%4y<z%1πf(πx1n,πy)\π1 if %3z = 0%1
\\πf(πx1n,π0)⊗x ... ⊗xπf(πx1n,πz-π1) if πz≥π0

\%gP%4y≤z%1πf(πx1n,πy) = %gP%4y<z+1%1πf(πx1n,πy)

.end
These bounded sums and products are functions of πx1n,πz. We can also define
doubly bounded sums and products in terms of the ones already given. For
example:

.BEGIN TABIT2(10,25);
\%GS%4u<y<v%1πf(πx1n,πy) \= πf(πx1n,πu1)+ ... +πf(πx1n,πz-πv1) 
\\%gS%4y<(v-u)-1%1πf(πx1n,πy+πu+π1)
.end

.BEGIN INDENT 0,10;
%7LEMMA 7%1 If πf(πx1n,πy) is PR (or R), then all the bounded sums and products
defined above are also PR (or R).
.begin tabit2(10,30);
Proof: Let πg(πx1n,πy) = %GS%4y<z%1πg(πx1n,πy).
Then:
\πg(πx1n,π0) \= π0
\πg(πx1n,πz1) =\πg(πx1n,πz)+\πf(πx1n,πz)
.end
The proofs of the others are quite similar.
.end
Given number-theoretic relations we can apply the connectives
of propositional logic to them to obtain new relations. We shall use
(∀πy)%4y<z%1πR(πx1n,πy) to express the relation: "for all πy, if πy is
less than πz, the πR(πx1n,πy) holds. We shall use (∀πy)%4y≤z%1, (∃πy)%4y<z%1,
and (∃πy)%4y≤z%1 in an analogous way. We call these %3bounded quatifiers%1.

In addition we define a %3bounded ?m%3-operator%1:
.begin tabit2(10,35);
\?mπy%4y<z%1πR(πx1n,πy) \= the least πy<πz for which πR(πx1n,πy) holds
\\   if there is such a πy.
\\πz otherwise
.end

.BEGIN INDENT 0,10;
%7THM 8%1 Relations obtained from PR (or R) relations by means of the propositonal
connectives and the bounded qunatifiers are also PR (or R). Also, applications
of the bounded ?m-operator, ?mπy%4y<z%1, leads from PR (or R) relations
to PR (or R) relations.

Proof: Assume πR1(πx1n) and πR2(πx1n) are PR-R relations. Then the characteristic
functions πCR1 and πCR2 are PR-R.

%3C%4~R1%1(πx1n) = π1-πCR1(πx1n); hence ~πR1 is PR-R. Also

%3C%4R1∨R2%1(πx1n) = πCR1(πx1n)⊗xπCR2(πx1n); hence πR1∨πR2 is PR-R. Since all of the
propositional connectives are definable in terms of ~ and ∨, this takes care
of all of them.

Now assume πR(πx1n) is PR-R. If %3Q%1(πx1n) is the relation
(∃πy)%4y<z%1πR(πx1n,πy), then πCQ(πx1n,πz)#=#%gP%4y<z%1πCR(πx1n,πy), which by
Lemma 7 is PR-R. 

The bounded quantifier
(∃πy)%4y≤z%1
is equivalent to
(∃πy)%4y<z+1%1,
which is obtainable from
(∃πy)%4y≤z%1
by substitution. Also
(∀πy)%4y<z%1
is equivalent to
~(∃πy)%4y<z%1~, and
(∀πy)%4y≤z%1
is equivalent to
~(∃πy)%4y≤z%1~.

Doubly bounded qunatifiers, such as
(∃πy)%4u<y<v%1 can be defined by substitution in the bounded qunatifiers
already mentioned.

Finally %gP%4u≤y%1πCR(πx1n,πu) has the value π1 for all πy such that
πR(πx1n) is false for all πu≤πy; it has the value π0 as soon as there is some
πu≤πy such that πR(πx1n,πu) holds. Hence %gS%4y<z%1(%gP%4u≤y%1πCR(πx1n,πu))
counts the number of integers from π0 up to but not including the first
πy<πz such that πR(πx1n,πy) holds and is πz if there is no such πy; thus it
is equal to ?mπy%4y<z%1πR(πx1n,πy) and so the latter function is PR-R
by lemma 7.
.end

For use in further study of recursive functions we
prove the following therem on definiton by cases⊗↓A forerunner of conditional
expressions.←.

.BEGIN INDENT 0,10;
%7THM 9%1  Let:

.BEGIN TABIT2(10,35);

\\πg1(πx1n) if πR1(πx1n) holds
\\πg2(πx1n) if πR2(πx1n) holds
\πf(πx1n) =\ ...
\\πgk(πx1n) if πRk(πx1n) holds

.end
If the functions πg1, ... πgk, and the relationa πR1, ... πRk are
PR-R, and if, for any πx1n, exactly one of the relations πR1(πx1n), ...,
πRk(πx1n) is true, then πf is PR-R.

Proof:

πf(πx1n) = πg1(πx1n)⊗x%3nsg%1(πCR1(πx1n))+ ...πgk(πx1n)⊗x%3nsg%1(πCRK(πx1n)).

.end